($\lambda$$E$,$x$,$z$. tree\_leaf($x$)) $\in$ $E$:Type$\rightarrow$$E$$\rightarrow\downarrow$True$\rightarrow$Tree($E$)